Tính đúng đắn của thuật toán có thể được chứng minh bằng quy nạp. Thuật toán có thể được phát biểu chính xác theo kiểu quy nạp như sau:

Bổ đề. Sau i lần lặp vòng for:

1. Nếu khoảng_cách(u) không có giá trị vô cùng lớn, thì nó bằng độ dài của một đường đi nào đó từ s tới u;
2. Nếu có một đường đi từ s tới u qua nhiều nhất i cung, thì Khoảng_cách(u) có giá trị không vượt quá độ dài của đường đi ngắn nhất từ s tới u qua tối đa i cung.

Chứng minh

Trường hợp cơ bản: Xét i = 0 và thời điểm trước khi vòng for được chạy lần đầu tiên. Khi đó, với đỉnh nguồn khoảng_cách(nguồn) = 0, điều này đúng. Đối với các đỉnh u khác, khoảng_cách(u) = vô cùng, điều này cũng đúng vì không có đường đi nào từ nguồn đến u qua 0 cung.

Trường hợp quy nạp:

Chứng minh câu 1. Xét thời điểm khi khoảng cách tới một đỉnh được cập nhật bởi công thứckhoảng_cách(v):= khoảng_cách(u) + trọng_số(u, v). Theo giả thiết quy nạp, khoảng_cách(u) là độ dài của một đường đi nào đó từ nguồn tới u. Do đó, khoảng_cách(u) + trọng_số(u, v) là độ dài của đường đi từ nguồn tới u rồi tới v.

Chứng minh câu 2: Xét đường đi ngắn nhất từ nguồn tới u qua tối đa i cung. Giả sử v là đỉnh liền ngay trước u trên đường đi này. Khi đó, phần đường đi từ nguồn tới v là đường đi ngắn nhất từ nguồn tới v qua tối đa i-1 cung. Theo giả thuyết quy nạp, khoảng_cách(v) sau i-1 vòng lặp không vượt quá độ dài đường đi này. Do đó, trọng_số(v, u) + khoảng_cách(v) có giá trị không vượt quá độ dài của đường đi từ s tới u. Trong lần lặp thứ i, khoảng_cách(u) được lấy giá trị nhỏ nhất của khoảng_cách(v) + trọng_số(v, u) với mọi v có thể. Do đó, sau i lần lặp, khoảng_cách(u) có giá trị không vượt quá độ dài đường đi ngắn nhất từ nguồn tới u qua tối đa i cung.

Khi i bằng số đỉnh của đồ thị, mỗi đường đi tìm được sẽ là đường đi ngắn nhất toàn cục, trừ khi đồ thị có chu trình âm. Nếu tồn tại chu trình âm mà từ đỉnh nguồn có thể đi đến được thì sẽ không tồn tại đường đi nhỏ nhất (vì mỗi lần đi quanh chu trình âm là một lần giảm trọng số của đường).